Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

Q is empty.


QTRS
  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS
  ↳ Non-Overlap Check
QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)


Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 4 less nodes.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
QDP
              ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
Used argument filtering: BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  x7
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  x7
newbuttons4(x1, x2, x3, x4)  =  newbuttons1(x4)
empty  =  empty
or2(x1, x2)  =  x2
true  =  true
false  =  false
Used ordering: Quasi Precedence: newbuttons_1 > true empty > true


↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPAfsSolverProof
QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPAfsSolverProof
                ↳ QDP
                  ↳ DependencyGraphProof
QDP

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.